x, y:Id, k:Knd, A, B, T:Type, f:(ABTA).
y = x  ma-single-effect1(x;A;y;B;k;T;f)  MsgA 

latex

Definitions	KindDeq, False, P  Q, Top, Unit, P  Q, P & Q, x  dom(f), , b, b, P  Q, MsgA, A, Prop, ma-single-effect1(x;A;y;B;k;T;f), with declarations ds:dsda:daeffect of k(v) is x := f s v, x. t(x), Valtype(da;k), Knd, State(ds), f  g, IdDeq, x : v, Id, x:A. B(x), f(x)?z, t  T
Lemmas	ma-state wf, ma-valtype wf, Knd wf, fpf-single wf, id-deq wf, Id wf, fpf-join wf, ma-single-effect wf, not wf, fpf-cap-single1, assert wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, fpf-join-cap-sq, fpf-single-dom, Kind-deq wf, subtype rel self